$\forall$$n$, $m$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$), $x$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. $f$[$n$:=$x$] $\in$ $\mathbb{N}$$_{\mbox{\scriptsize $<$$n$+1}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$